package tr.edu.ege.kipler.satisfiability.container;

import java.util.Iterator;
import java.util.Set;

import tr.edu.ege.kipler.common.Copyable;
import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.syntax.Role;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.ObjectRoleAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.SameIndividualAssertion;

/**
 * 
 * @author İnanç Seylan
 *
 */
public interface ABox extends FormulaBase, Copyable<ABox> {

	public void add(ConceptAssertion ca) throws UnsatisfiableException;

	public void add(ObjectRoleAssertion ra) throws UnsatisfiableException;

	public void add(SameIndividualAssertion assertion)
			throws UnsatisfiableException;

	public boolean contains(SameIndividualAssertion ia);

	public boolean contains(ConceptAssertion ca);

	public boolean contains(ObjectRoleAssertion ra);

	public boolean contains(String individual);

	public boolean containsEdge(Role role, Individual from, Individual to);

	public boolean containsEdge(Individual node, Individual succCandidate);

	public void remove(String name);

	public Iterator<Individual> predecessorIterator(Individual filler);

	public Iterator<Individual> successorIterator(Individual owner);

	public Iterator<Individual> neighborIterator(Individual indv);

	public Iterator<ObjectRoleAssertion> predecessorIterator(Role role,
			Individual filler);

	public Iterator<ObjectRoleAssertion> successorIterator(Role role,
			Individual owner);

	public Iterator<ObjectRoleAssertion> neighborIterator(Role role,
			Individual owner);

	public Set<Role> getEdges(Individual owner, Individual filler);

	public Iterator<Individual> differentIndividualIterator(
			Individual individual);

	public Iterator<Individual> sameIndividualIterator(Individual individual);

	public Individual getIndividual(String name);

	public Iterator<Individual> individualIterator();

	public World getWorld();

	public void setWorld(World world);
	
	public void setHasClash(boolean hasClash);
}
